FDL - Step of Proof: comp_nat_ind_tp

Step of Proof: comp_nat_ind_tp

Inference at *
Iof proof for Lemma comp nat ind tp:

P:(

{k}). (

i:

. (

j:

. (j < i)

P(j))

P(i))

{

i:

. P(i)}

by ((UnivCD)

CollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n

C)) (first_tok :t) inil_term)))

C1:

C1: 1. P :

{k}

C1: 2.

i:

. (

j:

. (j < i)

P(j))

P(i)

C1:

i:

. P(i)

C.

Definitions t T, {T}, x(s), P Q, , x:A. B(x),

Lemmas nat wf